Nuprl Definition : ma-has-pre
11,40
postcript
pdf
a
in dom(
M
.pre) ==
a
dom((
M
.2.2.2).1)
latex
clarification:
a
in dom(
M
.pre) ==
fpf-dom(IdDeq;
a
; ((
M
.2.2.2).1))
latex
Definitions
t
.2
,
t
.1
,
IdDeq
,
x
dom(
f
)
,
b
FDL editor aliases
ma-has-pre
origin
a 
dom((M.2.2.2).1)
fpf-dom(IdDeq; a; ((M.2.2.2).1)) a dom((M.2.2.2).1)
fpf-dom(IdDeq; a; ((M.2.2.2).1)) dom(f)b